(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
mark(s(div(s(x2347_1), s(y3881_1)))) →+ s(if_active(ge_active(mark(x2347_1), y3881_1), s(div(minus(mark(x2347_1), y3881_1), s(y3881_1))), 0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0].
The pumping substitution is [x2347_1 / s(div(s(x2347_1), s(y3881_1)))].
The result substitution is [ ].
The rewrite sequence
mark(s(div(s(x2347_1), s(y3881_1)))) →+ s(if_active(ge_active(mark(x2347_1), y3881_1), s(div(minus(mark(x2347_1), y3881_1), s(y3881_1))), 0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0,0].
The pumping substitution is [x2347_1 / s(div(s(x2347_1), s(y3881_1)))].
The result substitution is [ ].
(2) BOUNDS(2^n, INF)